
(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

let rec app l m =
  match l with
  | [] -> m
  | a::l1 -> a::(app l1 m)

(** val hd : 'a1 -> 'a1 list -> 'a1 **)

let hd default = function
| [] -> default
| x::_ -> x

(** val tl : 'a1 list -> 'a1 list **)

let tl = function
| [] -> []
| _::m -> m

type 'a mat =
  'a list list
  (* singleton inductive, whose constructor was mkMat *)

(** val mat0 : int -> int -> 'a1 mat -> 'a1 list list **)

let mat0 _ _ m =
  m

(** val nil_list : int -> 'a1 list list **)

let rec nil_list m =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> [])
    (fun n -> []::(nil_list n))
    m

(** val list_map : ('a1 -> 'a1) -> 'a1 list -> 'a1 list **)

let rec list_map f = function
| [] -> []
| x::x' -> (f x)::(list_map f x')

(** val list_each :
    ('a1 -> 'a1 -> 'a1) -> 'a1 list -> 'a1 list -> 'a1 list **)

let rec list_each f l1 l2 =
  match l1 with
  | [] -> []
  | hd1::tl1 ->
    (match l2 with
     | [] -> []
     | hd2::tl2 -> (f hd1 hd2)::(list_each f tl1 tl2))

(** val product' :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 list -> 'a1 list
    -> 'a1 **)

let rec product' zero add mul l1 l2 =
  match l1 with
  | [] -> zero
  | h1::t1 ->
    (match l2 with
     | [] -> zero
     | h2::t2 -> add (mul h1 h2) (product' zero add mul t1 t2))

(** val list_o : 'a1 -> int -> 'a1 list **)

let rec list_o zero n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> [])
    (fun n' -> zero::(list_o zero n'))
    n

(** val dlist_o : 'a1 -> int -> int -> 'a1 list list **)

let rec dlist_o zero m n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> [])
    (fun m' -> (list_o zero n)::(dlist_o zero m' n))
    m

(** val mO : 'a1 -> int -> int -> 'a1 mat **)

let mO =
  dlist_o

(** val dlist_map : ('a1 -> 'a1) -> 'a1 list list -> 'a1 list list **)

let rec dlist_map f = function
| [] -> []
| l::m' -> (list_map f l)::(dlist_map f m')

(** val matrix_map' :
    ('a1 -> 'a1) -> int -> int -> 'a1 mat -> 'a1 list list **)

let matrix_map' f m n ma =
  let m' = mat0 m n ma in dlist_map f m'

(** val matrix_map : ('a1 -> 'a1) -> int -> int -> 'a1 mat -> 'a1 mat **)

let matrix_map =
  matrix_map'

(** val mat_each' :
    ('a1 -> 'a1 -> 'a1) -> 'a1 list list -> 'a1 list list -> 'a1 list list **)

let rec mat_each' f1 left right =
  match left with
  | [] -> []
  | a::o ->
    (match right with
     | [] -> []
     | b::p -> (list_each f1 a b)::(mat_each' f1 o p))

(** val mat_each :
    ('a1 -> 'a1 -> 'a1) -> int -> int -> 'a1 mat -> 'a1 mat -> 'a1 list list **)

let mat_each f1 m n left right =
  let l = mat0 m n left in let r = mat0 m n right in mat_each' f1 l r

(** val matrix_each :
    ('a1 -> 'a1 -> 'a1) -> int -> int -> 'a1 mat -> 'a1 mat -> 'a1 mat **)

let matrix_each =
  mat_each

(** val headcolumn : 'a1 -> 'a1 list list -> 'a1 list **)

let rec headcolumn zero = function
| [] -> []
| x::x' -> (hd zero x)::(headcolumn zero x')

(** val tailcolumn : 'a1 list list -> 'a1 list list **)

let rec tailcolumn = function
| [] -> []
| x::x' -> (tl x)::(tailcolumn x')

(** val gettrans : 'a1 -> 'a1 list list -> int -> 'a1 list list **)

let rec gettrans zero m n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> nil_list n)
    (fun n' -> (headcolumn zero m)::(gettrans zero (tailcolumn m) n'))
    n

(** val trans : 'a1 -> int -> int -> 'a1 mat -> 'a1 mat **)

let trans zero m n ma =
  gettrans zero (mat0 m n ma) n

(** val mlink : 'a1 list list -> 'a1 list list -> 'a1 list list **)

let rec mlink ma mb =
  match ma with
  | [] -> mb
  | x::x' -> (match mb with
              | [] -> ma
              | y::y' -> (app x y)::(mlink x' y'))

(** val l_mul_dl :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 list -> 'a1 list
    list -> 'a1 list **)

let rec l_mul_dl zero add mul l = function
| [] -> []
| a::t -> (product' zero add mul l a)::(l_mul_dl zero add mul l t)

(** val dl_mul_dl :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> 'a1 list list -> 'a1
    list list -> 'a1 list list **)

let rec dl_mul_dl zero add mul left right =
  match left with
  | [] -> []
  | a::t -> (l_mul_dl zero add mul a right)::(dl_mul_dl zero add mul t right)

(** val mat_mul_mat :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    'a1 mat -> 'a1 mat -> 'a1 list list **)

let mat_mul_mat zero add mul m n p left right =
  let l1 = mat0 m n left in
  let right' = trans zero n p right in
  let l2 = mat0 p n right' in dl_mul_dl zero add mul l1 l2

(** val matrix_mul :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    'a1 mat -> 'a1 mat -> 'a1 mat **)

let matrix_mul =
  mat_mul_mat

(** val mf :
    int -> int -> ('a1 -> 'a1 -> 'a1) -> 'a1 mat -> 'a1 mat -> 'a1 mat **)

let mf m n f =
  matrix_each f m n

(** val lM_to_M1 : int -> int -> 'a1 mat list -> 'a1 list list **)

let rec lM_to_M1 m n = function
| [] -> nil_list m
| x::x' -> mlink (mat0 m n x) (lM_to_M1 m n x')

(** val dlM_to_M1 : int -> int -> 'a1 mat list list -> 'a1 list list **)

let rec dlM_to_M1 m n = function
| [] -> []
| x::x' -> app (lM_to_M1 m n x) (dlM_to_M1 m n x')

(** val mM_to_M' :
    int -> int -> int -> int -> 'a1 mat mat -> 'a1 list list **)

let mM_to_M' m n m2 n2 ma1 =
  let ma1' = mat0 m2 n2 ma1 in dlM_to_M1 m n ma1'

(** val mM_to_M : int -> int -> int -> int -> 'a1 mat mat -> 'a1 mat **)

let mM_to_M =
  mM_to_M'

(** val mZero : 'a1 -> int -> int -> 'a1 mat **)

let mZero =
  mO

(** val madd' :
    ('a1 -> 'a1 -> 'a1) -> int -> int -> 'a1 mat -> 'a1 mat -> 'a1 mat **)

let madd' add m p =
  mf m p add

(** val mmul :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    'a1 mat -> 'a1 mat -> 'a1 mat **)

let mmul =
  matrix_mul

(** val product :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    'a1 mat list -> 'a1 mat list -> 'a1 mat **)

let rec product zero add mul m n p l1 l2 =
  match l1 with
  | [] -> mZero zero m p
  | h1::t1 ->
    (match l2 with
     | [] -> mZero zero m p
     | h2::t2 ->
       madd' add m p (mmul zero add mul m n p h1 h2)
         (product zero add mul m n p t1 t2))

(** val mhead : 'a1 -> int -> int -> 'a1 mat list -> 'a1 mat **)

let mhead zero m n = function
| [] -> trans zero m n (mO zero m n)
| x::_ -> trans zero m n x

(** val mheadcolumn :
    'a1 -> int -> int -> 'a1 mat list list -> 'a1 mat list **)

let rec mheadcolumn zero m n = function
| [] -> []
| x::x' -> (mhead zero m n x)::(mheadcolumn zero m n x')

(** val mgettrans :
    'a1 -> int -> int -> 'a1 mat list list -> int -> 'a1 mat list list **)

let rec mgettrans zero m n ma n2 =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> [])
    (fun n' ->
    (mheadcolumn zero m n ma)::(mgettrans zero m n (tailcolumn ma) n'))
    n2

(** val mmtrans :
    'a1 -> int -> int -> int -> int -> 'a1 mat mat -> 'a1 mat mat **)

let mmtrans zero m n m2 n2 mma =
  mgettrans zero m n (mat0 m2 n2 mma) n2

(** val ml_mul_dl :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    'a1 mat list -> 'a1 mat list list -> 'a1 mat list **)

let rec ml_mul_dl zero add mul m n p l = function
| [] -> []
| a::t -> (product zero add mul m n p l a)::(ml_mul_dl zero add mul m n p l t)

(** val mdl_mul_dl :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    'a1 mat list list -> 'a1 mat list list -> 'a1 mat list list **)

let rec mdl_mul_dl zero add mul m n p left right =
  match left with
  | [] -> []
  | a::t ->
    (ml_mul_dl zero add mul m n p a right)::(mdl_mul_dl zero add mul m n p t
                                              right)

(** val mmat_mul_mat :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    int -> int -> int -> 'a1 mat mat -> 'a1 mat mat -> 'a1 mat list list **)

let mmat_mul_mat zero add mul m n p m2 n2 p2 left right =
  let l1 = mat0 m2 n2 left in
  let right' = trans (mO zero n p) n2 p2 right in
  let l2 = mat0 p2 n2 right' in mdl_mul_dl zero add mul m n p l1 l2

(** val mmatrix_mul :
    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> int -> int -> int ->
    int -> int -> int -> 'a1 mat mat -> 'a1 mat mat -> 'a1 mat mat **)

let mmatrix_mul =
  mmat_mul_mat

(** val mmatrix_each :
    int -> int -> ('a1 -> 'a1 -> 'a1) -> int -> int -> 'a1 mat mat -> 'a1 mat
    mat -> 'a1 mat mat **)

let mmatrix_each m n f =
  matrix_each (matrix_each f m n)

(** val mmatrix_map :
    int -> int -> ('a1 -> 'a1) -> int -> int -> 'a1 mat mat -> 'a1 mat mat **)

let mmatrix_map m n f =
  matrix_map (matrix_map f m n)
